Nuprl Lemma : antecedent-surjection_functionality_wrt_iff 11,40
es:ES, P1, P2, Q1, Q2:(E), f:({e:E| P1(e)} {e:E| Q1(e)} ).
(e:E. (P1(e))  (P2(e)))
 (e:E. (Q1(e))  (Q2(e)))
 (Q1  f P1  Q2  f P2) 
latex

Definitionsx:A. B(x), A c B, t  T, Q f P, P  Q, P & Q, Q  f P, P  Q, P  Q, , x:A. B(x)
Lemmasevent system wf, iff wf, es-E wf, subtype rel function, antecedent-surjection wf

origin